Iof proof for Lemma lt int eq false elim sqequal:
i, j:
. (i <z j ~ ff) 
(
(i < j))
by (RepeatFor 2 ((D 0)
THENW ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
T)) (first_tok :t) inil_term)))
)
T1:
T1: 1. i :
T1: 2. j :
T1: (i <z j ~ ff) ((i < j))
T.
T